Inference at * 2 2 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. 0 < ||L1||
7. 0 < ||L2||
8. x = last(L1)
9. y = hd(L2)
  x = (L1 @ L2)[(||L1|| - 1)] 

latex

 by ((RWO "select_append_front" 0) 
CollapseTHEN (Auto')) 

latex

C1: 

C1:   x = L1[(||L1|| - 1)]
C.

Definitions	P  Q, P  Q, i  j < k, P & Q, x:A  B(x), t  T, , {x:A| B(x)} , x:A. B(x), A  B, A, False, P  Q, x:AB(x), Void, , {i..j}, hd(l), l[i], n - m, #$n, last(L), a < b, type List, Type, s = t, ||as||, i  j
Lemmas	iff wf, rev implies wf, select append front, nat wf, member wf, le wf